h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))
↳ QTRS
↳ DependencyPairsProof
h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))
H(c(s(x), c(s(0), y)), z) → H(y, c(s(0), c(x, z)))
H(x, c(y, z)) → H(c(s(y), x), z)
h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
H(c(s(x), c(s(0), y)), z) → H(y, c(s(0), c(x, z)))
H(x, c(y, z)) → H(c(s(y), x), z)
h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(c(s(x), c(s(0), y)), z) → H(y, c(s(0), c(x, z)))
Used ordering: Polynomial interpretation [25,35]:
H(x, c(y, z)) → H(c(s(y), x), z)
The value of delta used in the strict ordering is 16.
POL(c(x1, x2)) = (4)x_1 + x_2
POL(s(x1)) = (1/2)x_1
POL(0) = 4
POL(H(x1, x2)) = (4)x_1 + (2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
H(x, c(y, z)) → H(c(s(y), x), z)
h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
H(x, c(y, z)) → H(c(s(y), x), z)
The value of delta used in the strict ordering is 6.
POL(c(x1, x2)) = 4 + (4)x_1 + (3/2)x_2
POL(s(x1)) = 5/2 + (4)x_1
POL(H(x1, x2)) = (3/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
h(x, c(y, z)) → h(c(s(y), x), z)
h(c(s(x), c(s(0), y)), z) → h(y, c(s(0), c(x, z)))